\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$, $y$:Id, $T_{1}$, $T_{2}$:Type, ${\it ks}_{1}$, ${\it ks}_{2}$:(Knd List),\+
\\[0ex]${\it tr}_{1}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}_{1}$)\} $\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T_{1}$$\rightarrow$$T_{1}$),
\\[0ex]${\it tr}_{2}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}_{2}$)\} $\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T_{2}$$\rightarrow$$T_{2}$).
\-\\[0ex]($\neg$($x$ = $y$))
\\[0ex]$\Rightarrow$ ${\it ds}$ $\parallel$ $x$ : $T_{1}$
\\[0ex]$\Rightarrow$ ${\it ds}$ $\parallel$ $y$ : $T_{2}$
\\[0ex]$\Rightarrow$ R{-}state{-}var($i$;${\it ds}$;${\it da}$;$x$;$T_{1}$;${\it ks}_{1}$;${\it tr}_{1}$) $\parallel$ R{-}state{-}var($i$;${\it ds}$;${\it da}$;$y$;$T_{2}$;${\it ks}_{2}$;${\it tr}_{2}$)
\end{tabbing}